-- Copyright 2012-2021, Microsoft Research, Daan Leijen.
--
-- This is free software; you can redistribute it and/or modify it under the
-- terms of the Apache License, Version 2.0. A copy of the License can be
-- found in the LICENSE file at the root of this distribution.
-----------------------------------------------------------------------------
{-
    Definition of higher-ranked types and utility functions over them.
-}
-----------------------------------------------------------------------------
{-# LANGUAGE InstanceSigs #-}
module Type.Type (-- * Types
                    Type(..), Scheme, Sigma, Rho, Tau, Effect, InferType
                  , Flavour(..)
                  , DataInfo(..), DataKind(..), ConInfo(..), SynInfo(..)
                  , dataInfoIsOpen, dataInfoIsExtend, dataInfoIsLiteral
                  , conInfoSize, conInfoScanCount
                  , conInfoIsLazy, dataInfoIsLazy, conInfoLazyFip, lazyName
                  , eqType, eqTypes, elemType
                  -- Predicates
                  , splitTypeScheme, shallowSplitVars
                  -- ** Type atoms
                  , TypeVar(..), TypeCon(..), TypeSyn(..), SynonymRank
                  -- ** Accessors
                  , maxSynonymRank
                  , synonymRank, typeVarId, typeConName, typeSynName
                  , isBound, isSkolem, isMeta, isMonoType
                  -- ** Operations
                  , makeScheme
                  , quantifyType, applyType, tForall
                  , expandSyn
                  , canonicalForm, minimalForm
                  -- ** Standard types
                  , typeInt, typeBool, typeFun, typeVoid, typeInt32, typeEvIndex, typeSSizeT
                  , typeUnit, typeChar, typeString, typeFloat
                  , typeTuple, typeAny
                  , typeEv, isEvType, makeEvType, typeResumeContext
                  , effectExtend, effectExtends, effectEmpty, effectFixed, tconEffectExtend
                  , effectExtendNoDup, effectExtendNoDups
                  , extractEffectExtend
                  , extractOrderedEffect
                  , orderEffect, labelName, labelNameFull, labelNameEx
                  , isEffectEmpty, isEffectFixed, shallowEffectExtend, shallowExtractEffectExtend

                  , typeDivergent, typeTotal, typePartial, typePure
                  , typeList, typeVector, typeApp, typeRef --, typeNull
                  , typeOptional, typeMakeTuple
                  , typeCCtx, typeCCtxx, typeFieldAddr
                  , isOptional, makeOptionalType, unOptional
                  , typeReuse, typeLocal, isTypeLocal

                  , tconHandled, tconHandled1, wrapHandledFromDataEffect
                  -- , typeCps
                  , isEffectAsync, isAsyncFunction

                  -- , isDelay
                  -- ** Standard tests
                  , isTau, isRho, isTVar, isTCon
                  , tconTotal, tconList
                  , isTypeTotal
                  , isTypeBool, isTypeInt, isTypeString, isTypeChar
                  , isTypeUnit
                  , isTypeLocalVar
                  , isValueOperation, makeValueOperation

                  -- ** Trivial conversion
                  , IsType( toType)
                  -- ** Primitive
                  , isFun, splitFunType, splitFunScheme
                  , getTypeArities
                  , module Common.Name
                  ) where

import Lib.Trace
import Data.Maybe(isJust)
import Data.List( sortBy, find )

import Common.Name
import Common.NamePrim
import Common.Range
import Common.Id
import Common.Failure
import Common.Syntax
import Kind.Kind

{--------------------------------------------------------------------------
  Types
--------------------------------------------------------------------------}
-- | Types
data Type   = TForall  ![TypeVar] !Rho  -- ^ forall a b c. phi, psi => rho
                                             -- there is at least one variable
                                             -- every variable occurs at least once in rho
                                             -- variables are canonically ordered
                                             -- rho has kind *
            | TFun     ![(Name,Type)] !Effect !Type    -- ^ (x:a, y:b, z:c) -> m d
            | TCon     !TypeCon               -- ^ type constant (primitive, label, or newtype; not -> or =>)
            | TVar     !TypeVar               -- ^ type variable (cannot instantiate to -> or =>)
            | TApp     !Type ![Type]           -- ^ application of datatypes
            | TSyn     !TypeSyn ![Type] !Type   -- ^ type synonym indirection
                                             -- first [Type] list is the actual arguments
                                             -- final Type is the "real" type (expanded) (always has kind *)
            deriving (Show)

-- | Various synonyms of types
type Scheme = Type
type Sigma  = Type    -- polymorphic type
type Tau    = Type    -- monomorphic type
type Rho    = Type    -- unqualified type
type Effect = Tau

-- | An inference type can contain type variables of flavour 'Meta' or 'Skolem'
type InferType = Type

-- | Type variables are variables in a type and contain an identifier and
-- kind. One can ask for the free type variables in a type, and substitute them with 'Tau' types.
data TypeVar = TypeVar{ typevarId :: !Id
                      , typevarKind :: !Kind
                      , typevarFlavour :: !Flavour
                      }
                      deriving (Show)

-- | The flavour of a type variable. Types in a "Type.Assumption" (Gamma) and inferred types in "Core.Core"
-- are always of the 'Bound' flavour. 'Meta' and 'Skolem' type variables only ever occur during type inference.
data Flavour = Meta | Skolem | Bound
             deriving (Eq, Ord, Show)

-- | Type constants have a name and a kind
data TypeCon = TypeCon{ typeconName :: !Name
                      , typeconKind :: !Kind
                      }
                      deriving (Show)

-- | Type synonyms have an identifier, kind, and rank (= partial ordering among type synonyms)
data TypeSyn = TypeSyn{ typesynName :: !Name
                      , typesynKind :: !Kind
                      , typesynRank :: !SynonymRank
                      , typesynInfo :: !(Maybe SynInfo)
                      }
                      deriving (Show)

-- | The rank of a type synonym gives a relative ordering among them. This is used
-- during unification to increase the chance of matching up type synonyms.
type SynonymRank = Int


maxSynonymRank :: Type -> SynonymRank
maxSynonymRank tp
  = case tp of
      TForall vars rho        -> maxSynonymRank rho
      TFun args eff tp        -> maxSynonymRanks (tp:eff:map snd args)
      TCon _                  -> 0
      TVar _                  -> 0
      TApp tp tps             -> maxSynonymRanks (tp:tps)
      TSyn syn args tp        -> max (synonymRank syn) (maxSynonymRanks (tp:args))

  where
    maxSynonymRanks tps
      = foldr max 0 (map maxSynonymRank tps)

{--------------------------------------------------------------------------
  Information about types

  Defined here to avoid circular dependencies
--------------------------------------------------------------------------}

-- | Data type information: name, kind, type arguments, and constructors
data DataInfo = DataInfo{ dataInfoSort    :: !DataKind
                        , dataInfoName    :: !Name
                        , dataInfoKind    :: !Kind
                        , dataInfoParams  :: ![TypeVar] {- ^ arguments -}
                        , dataInfoConstrs :: ![ConInfo]
                        , dataInfoRange   :: !Range
                        , dataInfoDef     :: !DataDef  -- value(raw,scan), normal, lazy, open, linear
                        , dataInfoEffect  :: !DataEffect
                        , dataInfoIsRec   :: !Bool     -- recursive datatype?
                        , dataInfoVis     :: !Visibility
                        , dataInfoDoc     :: !String
                        }


dataInfoIsExtend info
  = dataDefIsExtend (dataInfoDef info)

dataInfoIsOpen info
  = dataDefIsOpen (dataInfoDef info)

dataInfoIsLiteral info
  = let name = dataInfoName info
    in (name == nameTpInt || name == nameTpChar || name == nameTpString || name == nameTpFloat)

dataInfoIsLazy :: DataInfo -> Bool
dataInfoIsLazy dataInfo
  = dataDefIsLazy (dataInfoDef dataInfo)

lazyName :: DataInfo -> String -> Name
lazyName info stem
  = unqualify $ typeQualifiedName (dataInfoName info) ("lazy-" ++ stem)


-- | Constructor information: constructor name, name of the newtype, field types, and the full type of the constructor
data ConInfo = ConInfo{ conInfoName :: !Name
                      , conInfoTypeName :: !Name
                      -- , conInfoTypeSort :: Name
                      , conInfoForalls:: ![TypeVar] {- ^ quantifiers -}
                      , conInfoExists :: ![TypeVar] {- ^ existentials -}
                      , conInfoParams :: ![(Name,Type)] {- ^ field types -}
                      , conInfoType   :: !Scheme
                      , conInfoTypeSort :: !DataKind  -- ^ inductive, coinductive, retractive
                      , conInfoRange :: !Range
                      , conInfoParamRanges :: ![Range]
                      , conInfoParamVis    :: ![Visibility]
                      , conInfoSingleton :: !Bool -- ^ is this the only constructor of this type?
                      , conInfoOrderedParams :: ![(Name,Type)] -- ^ fields ordered by size
                      , conInfoValueRepr :: !ValueRepr
                      , conInfoLazy :: !(Maybe Fip)     -- also Just for indirection nodes
                      , conInfoTag :: !Int
                      , conInfoVis :: !Visibility
                      , conInfoDoc :: !String
                      }

instance Show ConInfo where
  show info
    = show (conInfoName info)

-- return size and scan count for a constructor
conInfoSize :: Platform -> ConInfo -> Int
conInfoSize platform conInfo
  = valueReprSize platform (conInfoValueRepr conInfo)

conInfoScanCount :: ConInfo -> Int
conInfoScanCount conInfo
  = valueReprScanCount (conInfoValueRepr conInfo)

conInfoIsLazy :: ConInfo -> Bool
conInfoIsLazy conInfo = isJust (conInfoLazy conInfo)

conInfoLazyFip :: ConInfo -> Fip
conInfoLazyFip conInfo
  = case conInfoLazy conInfo of
      Just fip -> fip
      Nothing  -> noFip

-- | A type synonym is quantified by type parameters
data SynInfo = SynInfo{ synInfoName :: Name
                      , synInfoKind  :: Kind
                      , synInfoParams ::  [TypeVar] {- ^ parameters -}
                      , synInfoType :: Type {- ^ result type -}
                      , synInfoRank :: SynonymRank
                      , synInfoRange :: Range
                      , synInfoVis :: Visibility
                      , synInfoDoc :: String
                      }
             deriving Show




{--------------------------------------------------------------------------
  Accessors
--------------------------------------------------------------------------}
-- | Return the 'Id' of a type variable
typeVarId :: TypeVar -> Id
typeVarId (TypeVar id kind _)  = id

typeConName :: TypeCon -> Name
typeConName (TypeCon name kind)      = name

typeSynName :: TypeSyn -> Name
typeSynName (TypeSyn name kind srank _) = name

-- | Return the relative /rank/ of a type synonym.
synonymRank :: TypeSyn -> SynonymRank
synonymRank (TypeSyn name kind srank _) = srank


-- | Is a type variable 'Bound'
isBound :: TypeVar -> Bool
isBound tv   = typevarFlavour tv == Bound

-- | Is a type variable 'Meta' (eg. unifiable)
isMeta :: TypeVar -> Bool
isMeta tv = typevarFlavour tv == Meta

-- | Is a type variable a 'Skolem' (eq. not unifiable)
isSkolem :: TypeVar -> Bool
isSkolem tv = typevarFlavour tv == Skolem

isMonoType :: Type -> Bool
isMonoType tp
  = case expandSyn tp of
      TForall{} -> False
      _         -> True


{--------------------------------------------------------------------------
  Equality
--------------------------------------------------------------------------}

instance Eq TypeVar where
  tv1 == tv2  = (typeVarId tv1 == typeVarId tv2) -- && (typevarFlavour tv1 == typevarFlavour tv2)

instance Ord TypeVar where
  -- tv1 <  tv2      = (typeVarId tv1 < typeVarId tv2) || (typeVarId tv)
  -- tv1 <= tv2      = (typeVarId tv1 <= typeVarId tv2)
  compare tv1 tv2 = case compare (typeVarId tv1) (typeVarId tv2) of
                      -- EQ   -> compare (typevarFlavour tv1) (typevarFlavour tv2)
                      ltgt -> ltgt



instance Eq TypeCon where
  tc1 == tc2      = (typeConName tc1 == typeConName tc2)

instance Ord TypeCon where
  tc1 <  tc2      = (typeConName tc1 < typeConName tc2)
  tc1 <= tc2      = (typeConName tc1 <= typeConName tc2)
  compare tc1 tc2 = compare (typeConName tc1) (typeConName tc2)


instance Eq TypeSyn where
  ts1 == ts2      = (typeSynName ts1 == typeSynName ts2)

instance Ord TypeSyn where
  ts1 <  ts2      = (typeSynName ts1 < typeSynName ts2)
  ts1 <= ts2      = (typeSynName ts1 <= typeSynName ts2)
  compare ts1 ts2 = compare (typeSynName ts1) (typeSynName ts2)

{--------------------------------------------------------------------------
  Split/add quantifiers
--------------------------------------------------------------------------}

-- | Split type into a list of universally quantified
-- type variables, a list of predicates, and a rho-type
splitTypeScheme :: Type -> ([TypeVar], Rho)
splitTypeScheme tp
  = case tp of
      TForall vars rho      -> (vars, rho)
      TSyn _ _  tp | mustSplit tp -> splitTypeScheme tp
      otherwise                   -> ([], tp)
  where
    -- We must split a synonym if its expansion includes further quantifiers or predicates
    mustSplit :: Type -> Bool
    mustSplit tp
      = case tp of
          TForall _ _   -> True
          TSyn _ _ tp   -> mustSplit tp
          _             -> False

-- Find all quantified type variables, but do not expand synonyms
shallowSplitVars tp
  = case tp of
      TForall vars rho       -> (vars, rho)
      otherwise              -> ([], tp)

expandSyn :: Type -> Type
expandSyn (TSyn syn args tp)
  = expandSyn tp
expandSyn tp
  = tp


-- | A type in canonical form has no type synonyms and expanded effect types.
canonicalForm :: Type -> Type
canonicalForm tp
  = case tp of
      TSyn syn args t       -> canonicalForm t
      TForall vars t        -> TForall vars (canonicalForm t)
      TApp t ts             -> TApp (canonicalForm t) (map canonicalForm ts)
      TFun args eff res     -> TFun [(name,canonicalForm t) | (name,t) <- args] (orderEffect (canonicalForm eff)) (canonicalForm res)
      _ -> tp


-- | A type in minimal form is in canonical form but also has no named function arguments
minimalForm :: Type -> Type
minimalForm tp
  = case tp of
      TSyn syn args t       -> canonicalForm t
      TForall vars t        -> TForall vars (canonicalForm t)
      TApp t ts             -> TApp (canonicalForm t) (map canonicalForm ts)
      TFun args eff res     -> TFun [(nameListNil,canonicalForm t) | (_,t) <- args] (orderEffect (canonicalForm eff)) (canonicalForm res)
      _ -> tp


-- | Create a type scheme from a list quantifiers.
makeScheme :: [TypeVar] -> Rho -> Scheme
makeScheme vars rho
  = case splitTypeScheme rho of
      (vars0,t) -> tForall (vars ++ vars0) t

quantifyType :: [TypeVar] -> Scheme -> Scheme
quantifyType vars tp
  = case splitTypeScheme tp of
      (vars0,rho) -> tForall (vars ++ vars0) rho

tForall :: [TypeVar] -> Rho -> Scheme
tForall [] rho   = rho
tForall vars rho = TForall vars rho


applyType tp1 tp2
  = case tp1 of
      TApp tp tps
        -> TApp tp (tps ++ [tp2])
      TSyn _ _ tp | mustSplit tp
        -> applyType tp tp2
      _ -> TApp tp1 [tp2]
  where
    mustSplit tp
      = case tp of
          TApp _ _    -> True
          TSyn _ _ tp -> mustSplit tp
          _           -> False


getTypeArities :: Type -> (Int,Int)
getTypeArities tp
  = case splitFunScheme tp of
      Just (tvars,pars,eff,res) -> (length tvars, length pars)
      Nothing -> (0,0)

splitFunScheme :: Scheme -> Maybe ([TypeVar],[(Name,Tau)],Effect,Tau)
splitFunScheme tp
  = let (tvars, rho) = splitTypeScheme tp
    in case splitFunType rho of
         Just (pars,eff,res) -> Just (tvars,pars,eff,res)
         Nothing             -> Nothing


{--------------------------------------------------------------------------
  Assertions
--------------------------------------------------------------------------}
-- | Is this a type variable?
isTVar :: Type -> Bool
isTVar tp
  = case tp of
      TVar tv     -> True
      TSyn _ _ t  -> isTVar t
      _           -> False

-- | Is this a type constant
isTCon :: Type -> Bool
isTCon tp
  = case tp of
      TCon c     -> True
      TSyn _ _ t -> isTCon t
      _          -> False

-- | Verify that a type is a rho type
-- (i.e., no outermost quantifiers)
isRho :: Type -> Bool
isRho tp
  = case tp of
      TForall _ _   -> False
      TSyn    _ _ t -> isRho t
      _             -> True

-- | Verify that a type is a tau type
-- (i.e., no quantifiers anywhere)
isTau :: Type -> Bool
isTau tp
  = case tp of
      TForall _ _    -> False
      TFun xs e r    -> all (isTau . snd) xs && isTau e && isTau r -- TODO e should always be tau
      TCon    _      -> True
      TVar    _      -> True
      TApp    a b    -> isTau a && all isTau b
      TSyn    _ ts t -> isTau t

-- | is this a function type
isFun :: Type -> Bool
isFun tp
  = case splitFunType tp of
      Nothing -> False
      Just (args,effect,res) -> True

-- | split a function type in its arguments, effect, and result type
splitFunType :: Type -> Maybe ([(Name,Type)],Type,Type)
splitFunType tp
  = case tp of
      TFun args effect result
        -> return (args, effect, result)
      TSyn _ _ t
        -> splitFunType t
      _ -> Nothing


{--------------------------------------------------------------------------
  Primitive types
--------------------------------------------------------------------------}

-- | Type of integers (@Int@)
typeInt :: Tau
typeInt
  = TCon tconInt

tconInt = (TypeCon nameTpInt (kindStar))
isTypeInt (TCon tc) = tc == tconInt
isTypeInt _         = False

typeInt32 :: Tau
typeInt32
  = TCon (TypeCon nameTpInt32 kindStar)

typeEvIndex :: Tau
typeEvIndex
  = TSyn (TypeSyn nameTpEvIndex kindStar 0 Nothing) [] typeSSizeT

typeSSizeT :: Tau
typeSSizeT
  = TCon (TypeCon nameTpSSizeT kindStar)

-- | Type of floats
typeFloat :: Tau
typeFloat
  = TCon (TypeCon nameTpFloat (kindStar))

-- | Type of characters
typeChar :: Tau
typeChar
  = TCon tconChar

tconChar = (TypeCon nameTpChar (kindStar))
isTypeChar (TCon tc) = tc == tconChar
isTypeChar _         = False



-- | Type of strings
typeString :: Tau
typeString
  = TCon tconString

tconString = (TypeCon nameTpString (kindStar))
isTypeString (TCon tc) = tc == tconString
isTypeString _         = False


typeResumeContext :: Tau -> Effect -> Effect -> Tau -> Tau
typeResumeContext b e e0 r
  = TApp (TCon tcon) [b,e,e0,r]
  where
    tcon = TypeCon nameTpResumeContext (kindFun kindStar (kindFun kindEffect (kindFun kindEffect (kindFun kindStar kindStar))))

typeRef :: Tau
typeRef
  = TCon (TypeCon nameTpRef (kindFun kindHeap (kindFun kindStar kindStar)))


tconLocalVar = TypeCon nameTpLocalVar (kindFun kindHeap (kindFun kindStar kindStar))

isTypeLocalVar :: Tau -> Bool
isTypeLocalVar tp =
  case expandSyn tp of
    TApp (TCon (TypeCon name _)) [_,_]  -> name == nameTpLocalVar
    _ -> False


isValueOperation tp
  = case splitTypeScheme tp of
      (_,TApp (TCon (TypeCon name _)) [_,_]) -> name == nameTpValueOp
      _ -> False

makeValueOperation eff tp
  = TApp (TCon (TypeCon nameTpValueOp kind)) [eff,tp]
  where
    kind = kindFun kindEffect (kindFun kindStar kindStar)

orderEffect :: HasCallStack => Tau -> Tau
orderEffect tp
  = let (ls,tl) = extractOrderedEffect tp
    in foldr effectExtend tl ls




extractOrderedEffect :: Tau -> ([Tau],Tau)
extractOrderedEffect tp
  = let (labs,tl) = extractEffectExtend tp
        labss     = concatMap expand labs
        slabs     = (sortBy (\l1 l2 -> labelNameCompare (labelName l1) (labelName l2)) labss)
    in -- trace ("sorted: " ++ show (map labelName labss) ++ " to " ++ show (map labelName slabs)) $
       (slabs,tl)
  where
    expand l
      = let (ls,tl) = extractEffectExtend l
        in if (isEffectEmpty tl && not (null ls))
            then ls
            else [l]

labelName :: Tau -> Name
labelName tp
  = let (name,_,_) = (labelNameEx tp) in name

labelNameFull :: Tau -> Name
labelNameFull tp
  = let (name,i,_) = labelNameEx tp
    in postpend ("$" ++ show i) name



labelNameEx :: Tau -> (Name,Int,[Tau])
labelNameEx tp
  = case expandSyn tp of
      TCon tc -> (typeConName tc,0,[])
      TApp (TCon (TypeCon name _)) [htp] | (name == nameTpHandled || name == nameTpHandled1 || name == nameTpNHandled || name == nameTpNHandled1)
        -> labelNameEx htp -- use the handled effect name for handled<htp> types.
      TApp (TCon tc) targs@(TVar (TypeVar id kind Skolem) : _)  | isKindScope kind
        -> (typeConName tc, idNumber id, targs)
      TApp (TCon tc) targs  -> assertion ("non-expanded type synonym used as label") (typeConName tc /= nameEffectExtend) $
                               (typeConName tc,0,targs)
      _  -> failure "Type.Type.labelNameEx: label is not a constant"

typePartial :: Type
typePartial
  = TApp tconHandled [TCon (TypeCon nameTpPartial kindHandled)]

typeLocal :: Type
typeLocal
  = TCon (TypeCon nameTpLocal kindLocal)

isTypeLocal :: Type -> Bool
isTypeLocal tp
  = case expandSyn tp of
      TApp (TCon (TypeCon name _)) [_]  -> name == nameTpLocal
      _ -> False

-- typeCps :: Type
-- typeCps
--   = TApp tconHandled [TCon (TypeCon nameTpCps kindHandled)]

tconHandled :: Type
tconHandled = TCon $ TypeCon nameTpHandled kind
  where
    kind = kindFun kindHandled kindLabel

tconHandled1 :: Type
tconHandled1 = TCon $ TypeCon nameTpHandled1 kind
  where
    kind = kindFun kindHandled1 kindLabel

wrapHandledFromDataEffect :: HasCallStack => DataEffect -> Type -> Type
wrapHandledFromDataEffect (DataEffect named linear) eff
  = let name = makeTpHandled named linear
        kind = kindFun kindHandled kindLabel
    in TApp (TCon (TypeCon name kind)) [eff]
wrapHandledFromDataEffect (DataNoEffect) teff
  = teff


isAsyncFunction tp
  = let (_,rho) = splitTypeScheme tp
    in case splitFunType rho of
         Just (_,eff,_) -> let (ls,_) = extractEffectExtend eff
                           in any isEffectAsync ls
         _ -> False

isEffectAsync tp
  = case expandSyn tp of
      TForall _ rho    -> isEffectAsync rho
      TFun _ eff _    -> isEffectAsync eff
      TApp (TCon (TypeCon name _)) [t]
        | name == nameTpHandled -> isEffectAsync t
      TCon (TypeCon hxName _)
        -> hxName == nameTpAsync
      _ -> False

isEffectTyVar (TVar v) = isKindEffect $ typevarKind v
isEffectTyVar _        = False


effectEmpty :: Tau
effectEmpty
  = TCon (TypeCon nameEffectEmpty kindEffect)

isEffectEmpty :: HasCallStack => Tau -> Bool
isEffectEmpty tp
  = case expandSyn tp of
      TCon tc -> typeConName tc == nameEffectEmpty
      _       -> False


effectExtendNoDup :: HasCallStack => Tau -> Tau -> Tau
effectExtendNoDup label eff
  = let (ls,_) = extractEffectExtend label
    in if null ls
        then let (els,_) = extractEffectExtend eff
             in if isJust (find (\e -> eqType label e) els) --  (label `elem` els)
                 then eff
                 else appEffectExtend label eff
        else effectExtendNoDups ls eff

effectExtendNoDups :: HasCallStack => [Tau] -> Tau -> Tau
effectExtendNoDups labels eff
  = foldr effectExtendNoDup eff labels


effectExtend :: HasCallStack => Tau -> Tau -> Tau
effectExtend label eff
  = let (ls,tl) = extractEffectExtend label
    in if null ls
        then appEffectExtend label eff
        else effectExtends ls eff

tconEffectExtend :: TypeCon
tconEffectExtend
  = TypeCon nameEffectExtend (kindFun kindLabel (kindFun kindEffect kindEffect))

effectExtends :: HasCallStack => [Tau] -> Tau -> Tau
-- prevent over expansion of type syonyms here  (see also: Core.Parse.teffect)
effectExtends [lab@(TSyn (TypeSyn _ kind _ _) _ _)] eff  | isEffectEmpty eff && kind == kindEffect
  = lab
effectExtends labels eff
  = foldr effectExtend eff labels

effectFixed :: [Tau] -> Tau
effectFixed labels
  = effectExtends labels effectEmpty

isEffectFixed :: Tau -> Bool
isEffectFixed tp
  = isEffectEmpty (snd (extractEffectExtend tp))

extractEffectExtend :: HasCallStack => Tau -> ([Tau],Tau)
extractEffectExtend t
  = case expandSyn t of
      TApp (TCon tc) [l,e]  | typeConName tc == nameEffectExtend
        -> case extractEffectExtend e of
             (ls,tl) -> case extractLabel l of
                          ls0 -> (ls0 ++ ls, tl)
      _ -> ([],t)
  where
    extractLabel :: Tau -> [Tau]
    extractLabel l
      = -- trace ("extractLabel: " ++ show l) $
        case expandSyn l of
          TApp (TCon tc) [_,e] | typeConName tc == nameEffectExtend
            -> let (ls,tl) = extractEffectExtend l
               in assertion "label was not a fixed effect type alias" (isEffectFixed tl) $
                  ls
          _ -> [l]


shallowExtractEffectExtend :: Tau -> ([Tau],Tau)
shallowExtractEffectExtend t
  = case t of
      TApp (TCon tc) [l,e]  | typeConName tc == nameEffectExtend
        -> case shallowExtractEffectExtend e of
             (ls,tl) -> (l:ls, tl)
      _ -> ([],t)

shallowEffectExtend :: HasCallStack => Tau -> Tau -> Tau
shallowEffectExtend label eff
  -- We do not expand type synonyms in the label here by using the 'shallow' version of extract
  -- this means that type synonyms of kind E (ie. a fixed effect row) could stay around in
  -- the label (which should have kind X).
  -- We use this to keep type synonyms around longer -- but during unification we got to be
  -- careful to expand such synonyms
  = let (ls,tl) = shallowExtractEffectExtend label
    in if null ls
        then appEffectExtend label eff
        else effectExtends ls eff


appEffectExtend :: HasCallStack => Type -> Effect -> Effect
-- appEffectExtend label eff | isKindHandled (kindOf label)
--  =  TApp (TCon tconEffectExtend) [TApp tconHandled [label],eff]
appEffectExtend label eff
  = assertion ("label has not kind X: " ++ show (label,eff,kindOf (expandSyn label))) (hasKindLabel label)
    TApp (TCon tconEffectExtend) [label,eff]
  where
    hasKindLabel l
      = let k = kindOf (expandSyn l)
        in (k == kindLabel || k == kindEffect) -- || isKindHandled k || isKindHandled1 k)

kindOf :: HasCallStack => Tau -> Kind
kindOf tau
  = case tau of
      TForall _ tp   -> kindOf tp
      TFun _ _ _     -> kindStar
      TVar v         -> typevarKind v
      TCon c         -> typeconKind c
      TSyn syn xs tp -> typesynKind syn
      TApp tp args   -> kindApply args (kindOf tp)
  where
    kindApply [] k   = k
    kindApply (_:rest) (KApp (KApp arr k1) k2)  = kindApply rest k2
    kindApply args  k  = failure ("Type.Type.kindOf: illegal kind in application? " ++ show (k) ++ " to " ++ show args
                              ++ "\n  " ++ show tau)


typeDivergent :: Tau
typeDivergent
  = single nameTpDiv

single :: Name -> Effect
single name
  = effectExtend (TCon (TypeCon name kindLabel)) effectEmpty

typeTotal :: Tau
typeTotal
  = effectEmpty -- TCon tconTotal

tconTotal :: TypeCon
tconTotal
  = TypeCon nameEffectEmpty kindEffect

isTypeTotal :: Tau -> Bool
isTypeTotal (TCon tc) = (tc == tconTotal)
isTypeTotal _         = False

{-
typePartial :: Tau
typePartial
  = single nameTpPartial
-}

typePure :: Tau
typePure
  = effectFixed [typePartial,typeDivergent]


-- | Type of boolean (@Bool@)
typeBool :: Tau
typeBool
  = TCon tconBool

tconBool
  = TypeCon nameTpBool (kindStar)

isTypeBool (TCon tc) = tc == tconBool
isTypeBool _         = False

isTypeUnit (TCon tc) = tc == tconUnit
isTypeUnit _         = False


-- | Type of ctail
typeCCtx :: Tau -> Tau
typeCCtx tp
  = TSyn tsynCCtx [tp] (TApp typeCCtxx [tp,tp])

tsynCCtx :: TypeSyn
tsynCCtx
  = TypeSyn nameTpCCtx (kindFun kindStar kindStar) 0 Nothing

typeCCtxx :: Tau
typeCCtxx
  = TCon tconCCtxx

tconCCtxx :: TypeCon
tconCCtxx
  = TypeCon nameTpCCtxx (kindFun kindStar (kindFun kindStar kindStar))

-- | Type of cfield
typeFieldAddr :: Tau
typeFieldAddr
  = TCon tconFieldAddr

tconFieldAddr :: TypeCon
tconFieldAddr
  = TypeCon nameTpFieldAddr (kindFun kindStar kindStar)

-- | Type of vectors (@[]@)
typeVector :: Tau
typeVector
  = TCon (TypeCon nameTpVector (kindFun kindStar kindStar))

-- | Type of lists (@[]@)
typeList :: Tau
typeList
  = TCon tconList

tconList :: TypeCon
tconList
  = TypeCon nameTpList (kindFun kindStar kindStar)

-- typeNull :: Tau -> Tau
-- typeNull tp
--   = typeApp (TCon (TypeCon nameTpNull kindStar)) [tp]

-- | Type of evidence.
typeEv :: Tau
typeEv = TCon tconEv

tconEv :: TypeCon
tconEv = TypeCon nameTpEv (kindFun kindStar kindStar)

isEvType :: Tau -> Bool
isEvType (TCon tc) = tc == tconEv
isEvType _         = False

makeEvType :: Type -> Type
makeEvType arg = typeApp typeEv [arg]

-- | Create a function type. Can have zero arguments.
typeFun :: [(Name,Tau)] -> Tau -> Tau -> Tau
typeFun args effect result
  = TFun args effect result

-- | Create an application
typeApp :: Tau -> [Tau] -> Tau
typeApp t []            = t
typeApp (TApp t ts0) ts = TApp t (ts0 ++ ts)
typeApp t ts            = TApp t ts

-- | Empty record
typeUnit :: Tau
typeUnit
  = TCon tconUnit

tconUnit
  = TypeCon nameTpUnit kindStar

typeVoid :: Tau
typeVoid
  = TCon (TypeCon nameTpVoid kindStar)

typeReuse :: Tau
typeReuse
   = TCon (TypeCon nameTpReuse kindStar)

typeAny :: Tau
typeAny
  = TCon (TypeCon (nameTpAny) kindStar)

typeMakeTuple :: [Tau] -> Tau
typeMakeTuple tps
  = case tps of
      [] -> typeUnit
      [tp] -> tp
      _    -> typeApp (typeTuple (length tps)) tps

typeTuple :: Int -> Tau
typeTuple n
  = TCon (TypeCon (nameTpTuple n) ({-kindArrowN n-} kindFunN (replicate n kindStar) kindStar))

typeOptional :: Tau
typeOptional
  = TCon tconOptional

tconOptional :: TypeCon
tconOptional
  = (TypeCon nameTpOptional (kindFun kindStar kindStar))

isOptional :: Type -> Bool
isOptional tp
  = case expandSyn tp of
      TApp (TCon tc) [t] -> tc == tconOptional
      _ -> False

makeOptionalType :: Type -> Type
makeOptionalType tp
  = TApp typeOptional [tp]

unOptional :: Type -> Type
unOptional tp
  = case expandSyn tp of
      TApp (TCon tc) [t] | tc == tconOptional -> t
      _ -> tp

-- | Remove type synonym indirections.
pruneSyn :: Rho -> Rho
pruneSyn rho
  = case rho of
      TSyn syn args t -> pruneSyn t
      TApp t1 ts      -> TApp (pruneSyn t1) (map pruneSyn ts)
      _               -> rho


{--------------------------------------------------------------------------
  Conversion between types
--------------------------------------------------------------------------}
class IsType a where
  -- | Trivial conversion to a kind quantified type scheme
  toType :: a -> Type

instance IsType Type where
  toType tp
    = tp

instance IsType TypeVar where
  toType v
    = TVar v

instance IsType TypeCon where
  toType con
    = TCon con


{--------------------------------------------------------------------------
  Equality between types
--------------------------------------------------------------------------}
-- instance Eq Type where
--  (==) = eqType

elemType :: Type -> [Type] -> Bool
elemType t ts
  = isJust (find (eqType t) ts)

eqType :: HasCallStack => Type -> Type -> Bool
eqType tp1 tp2
  = case (expandSyn tp1,expandSyn tp2) of
      (TForall vs1 t1, TForall vs2 t2)          -> (vs1==vs2 && eqType t1 t2)
      (TFun pars1 eff1 t1, TFun pars2 eff2 t2)  -> (eqTypes (map snd pars1) (map snd pars2) && matchEffect eff1 eff2 && eqType t1 t2)
      (TCon c1, TCon c2)                        -> c1 == c2
      (TVar v1, TVar v2)                        -> v1 == v2
      (TApp t1 ts1, TApp t2 ts2)                -> (eqType t1 t2 && eqTypes ts1 ts2)
      -- (TSyn syn1 ts1 t1, TSyn syn2 ts2 t2)      -> (syn1 == syn2 && eqTypes ts1 ts2 && eqType t1 t2)
      _ -> False

matchEffect :: HasCallStack => Effect -> Effect -> Bool
matchEffect eff1 eff2
  = eqType (orderEffect eff1) (orderEffect eff2)

eqTypes :: HasCallStack => [Type] -> [Type] -> Bool
eqTypes ts1 ts2
  = and (zipWith eqType ts1 ts2)
